Nuprl Lemma : mux-component_wf 11,40
ds:(IdType), da:(IdKndType), Aa, Ba, Ab, Bb:Type, Ca:Component(ds;da;Aa;Ba),
Cb:Component(ds;da;Ab;Bb).
mux-component(Ca;Cb)  Component(ds;da;Aa + Ab;Ba + Bb) 
latex

DefinitionsTop, mux-component(Ca;Cb), t  T, Component(ds;da;A;B), x:A. B(x), P  Q
LemmasKnd wf, Id wf, RealizerScheme wf, interface wf, interface-union wf, scheme-plus wf, interface-right wf, subtype rel sum, top wf, interface-subtype, interface-left wf

origin